Nuprl Lemma : ma-rframe_wf
11,40
postcript
pdf
M
:MsgA,
k
:Knd,
x
:Id.
M
.rframe(
k
reads
x
)
latex
Definitions
MsgA
,
x
:
A
B
(
x
)
,
M
.rframe(
k
reads
x
)
,
z
!=
f
(
x
)
P
(
a
;
z
)
,
x
,
y
.
t
(
x
;
y
)
,
,
deq-member(
eq
;
x
;
L
)
,
KindDeq
,
{
x
:
A
|
B
(
x
)}
,
Type
,
b
,
x
dom(
f
)
,
IdDeq
,
x
:
A
B
(
x
)
,
a
:
A
fp
B
(
a
)
,
Top
,
x
.
t
(
x
)
,
x
:
A
.
B
(
x
)
,
x
.
A
(
x
)
,
type
List
,
Id
,
t
T
,
Knd
Lemmas
Knd
wf
,
Id
wf
,
fpf-trivial-subtype-top
,
id-deq
wf
,
fpf-dom
wf
,
assert
wf
,
Kind-deq
wf
,
deq-member
wf
,
fpf-val
wf
,
msga
wf
origin
M:MsgA, k:Knd, x:Id. M.rframe(k reads x) 
M:MsgA, k:Knd, x:Id. M.rframe(k reads x) 
B(x)
P(a;z)
x,y. t(x;y)
b dom(f)
B(x) B(a)x. t(x)x:A. B(x)x.A(x) T